define("ace/mode/doc_comment_highlight_rules", ["require", "exports", "module", "ace/lib/oop", "ace/mode/text_highlight_rules"], function (require, exports, module) {
    "use strict";

    var oop = require("../lib/oop");
    var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;

    var DocCommentHighlightRules = function () {
        this.$rules = {
            "start": [{
                token: "comment.doc.tag",
                regex: "@[\\w\\d_]+" // TODO: fix email addresses
            },
                DocCommentHighlightRules.getTagRule(),
                {
                    defaultToken: "comment.doc",
                    caseInsensitive: true
                }]
        };
    };

    oop.inherits(DocCommentHighlightRules, TextHighlightRules);

    DocCommentHighlightRules.getTagRule = function (start) {
        return {
            token: "comment.doc.tag.storage.type",
            regex: "\\b(?:TODO|FIXME|XXX|HACK)\\b"
        };
    };

    DocCommentHighlightRules.getStartRule = function (start) {
        return {
            token: "comment.doc", // doc comment
            regex: "\\/\\*(?=\\*)",
            next: start
        };
    };

    DocCommentHighlightRules.getEndRule = function (start) {
        return {
            token: "comment.doc", // closing comment
            regex: "\\*\\/",
            next: start
        };
    };


    exports.DocCommentHighlightRules = DocCommentHighlightRules;

});

define("ace/mode/lean_highlight_rules", ["require", "exports", "module", "ace/lib/oop", "ace/mode/doc_comment_highlight_rules", "ace/mode/text_highlight_rules"], function (require, exports, module) {
    "use strict";

    var oop = require("../lib/oop");
    var DocCommentHighlightRules = require("./doc_comment_highlight_rules").DocCommentHighlightRules;
    var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;

    var leanHighlightRules = function () {

        var keywordControls = (
            ["add_rewrite", "alias", "as", "assume", "attribute",
                "begin", "by", "calc", "calc_refl", "calc_subst", "calc_trans", "check",
                "classes", "coercions", "conjecture", "constants", "context",
                "corollary", "else", "end", "environment", "eval", "example",
                "exists", "exit", "export", "exposing", "extends", "fields", "find_decl",
                "forall", "from", "fun", "have", "help", "hiding", "if",
                "import", "in", "infix", "infixl", "infixr", "instances",
                "let", "local", "match", "namespace", "notation", "obtain", "obtains",
                "omit", "opaque", "open", "options", "parameter", "parameters", "postfix",
                "precedence", "prefix", "premise", "premises", "print", "private", "proof",
                "protected", "qed", "raw", "renaming", "section", "set_option",
                "show", "tactic_hint", "take", "then", "universe",
                "universes", "using", "variable", "variables", "with"].join("|")
        );

        var nameProviders = (
            ["inductive", "structure", "record", "theorem", "axiom",
                "axioms", "lemma", "hypothesis", "definition", "constant"].join("|")
        );

        var storageType = (
            ["Prop", "Type", "Type'", "Type₊", "Type₁", "Type₂", "Type₃"].join("|")
        );

        var storageModifiers = (
            "\\[(" +
            ["abbreviations", "all-transparent", "begin-end-hints", "class", "classes", "coercion",
                "coercions", "declarations", "decls", "instance", "irreducible",
                "multiple-instances", "notation", "notations", "parsing-only", "persistent",
                "reduce-hints", "reducible", "tactic-hints", "visible", "wf", "whnf"
            ].join("|") +
            ")\\]"
        );

        var keywordOperators = (
            [].join("|")
        );

        var keywordMapper = this.$keywords = this.createKeywordMapper({
            "keyword.control": keywordControls,
            "storage.type": storageType,
            "keyword.operator": keywordOperators,
            "variable.language": "sorry"
        }, "identifier");

        var identifierRe = "[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f][A-Za-z0-9_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079\u207f-\u2089\u2090-\u209c\u2100-\u214f]*";
        var operatorRe = new RegExp(["#", "@", "->", "∼", "↔", "/", "==", "=", ":=", "<->",
            "/\\", "\\/", "∧", "∨", "≠", "<", ">", "≤", "≥", "¬",
            "<=", ">=", "⁻¹", "⬝", "▸", "\\+", "\\*", "-", "/",
            "λ", "→", "∃", "∀", ":="].join("|"));

        this.$rules = {
            "start": [
                {
                    token: "comment", // single line comment "--"
                    regex: "--.*$"
                },
                DocCommentHighlightRules.getStartRule("doc-start"),
                {
                    token: "comment", // multi line comment "/-"
                    regex: "\\/-",
                    next: "comment"
                }, {
                    stateName: "qqstring",
                    token: "string.start", regex: '"', next: [
                        {token: "string.end", regex: '"', next: "start"},
                        {token: "constant.language.escape", regex: /\\[n"\\]/},
                        {defaultToken: "string"}
                    ]
                }, {
                    token: "keyword.control", regex: nameProviders, next: [
                        {token: "variable.language", regex: identifierRe, next: "start"}]
                }, {
                    token: "constant.numeric", // hex
                    regex: "0[xX][0-9a-fA-F]+(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
                }, {
                    token: "constant.numeric", // float
                    regex: "[+-]?\\d+(?:(?:\\.\\d*)?(?:[eE][+-]?\\d+)?)?(L|l|UL|ul|u|U|F|f|ll|LL|ull|ULL)?\\b"
                }, {
                    token: "storage.modifier",
                    regex: storageModifiers
                }, {
                    token: keywordMapper,
                    regex: identifierRe
                }, {
                    token: "operator",
                    regex: operatorRe
                }, {
                    token: "punctuation.operator",
                    regex: "\\?|\\:|\\,|\\;|\\."
                }, {
                    token: "paren.lparen",
                    regex: "[[({]"
                }, {
                    token: "paren.rparen",
                    regex: "[\\])}]"
                }, {
                    token: "text",
                    regex: "\\s+"
                }
            ],
            "comment": [{token: "comment", regex: "-/", next: "start"},
                {defaultToken: "comment"}]
        };

        this.embedRules(DocCommentHighlightRules, "doc-",
            [DocCommentHighlightRules.getEndRule("start")]);
        this.normalizeRules();
    };

    oop.inherits(leanHighlightRules, TextHighlightRules);

    exports.leanHighlightRules = leanHighlightRules;
});

define("ace/mode/matching_brace_outdent", ["require", "exports", "module", "ace/range"], function (require, exports, module) {
    "use strict";

    var Range = require("../range").Range;

    var MatchingBraceOutdent = function () {
    };

    (function () {

        this.checkOutdent = function (line, input) {
            if (!/^\s+$/.test(line))
                return false;

            return /^\s*\}/.test(input);
        };

        this.autoOutdent = function (doc, row) {
            var line = doc.getLine(row);
            var match = line.match(/^(\s*\})/);

            if (!match) return 0;

            var column = match[1].length;
            var openBracePos = doc.findMatchingBracket({row: row, column: column});

            if (!openBracePos || openBracePos.row == row) return 0;

            var indent = this.$getIndent(doc.getLine(openBracePos.row));
            doc.replace(new Range(row, 0, row, column - 1), indent);
        };

        this.$getIndent = function (line) {
            return line.match(/^\s*/)[0];
        };

    }).call(MatchingBraceOutdent.prototype);

    exports.MatchingBraceOutdent = MatchingBraceOutdent;
});

define("ace/mode/lean", ["require", "exports", "module", "ace/lib/oop", "ace/mode/text", "ace/mode/lean_highlight_rules", "ace/mode/matching_brace_outdent", "ace/range"], function (require, exports, module) {
    "use strict";

    var oop = require("../lib/oop");
    var TextMode = require("./text").Mode;
    var leanHighlightRules = require("./lean_highlight_rules").leanHighlightRules;
    var MatchingBraceOutdent = require("./matching_brace_outdent").MatchingBraceOutdent;
    var Range = require("../range").Range;

    var Mode = function () {
        this.HighlightRules = leanHighlightRules;

        this.$outdent = new MatchingBraceOutdent();
    };
    oop.inherits(Mode, TextMode);

    (function () {

        this.lineCommentStart = "--";
        this.blockComment = {start: "/-", end: "-/"};

        this.getNextLineIndent = function (state, line, tab) {
            var indent = this.$getIndent(line);

            var tokenizedLine = this.getTokenizer().getLineTokens(line, state);
            var tokens = tokenizedLine.tokens;
            var endState = tokenizedLine.state;

            if (tokens.length && tokens[tokens.length - 1].type == "comment") {
                return indent;
            }

            if (state == "start") {
                var match = line.match(/^.*[\{\(\[]\s*$/);
                if (match) {
                    indent += tab;
                }
            } else if (state == "doc-start") {
                if (endState == "start") {
                    return "";
                }
                var match = line.match(/^\s*(\/?)\*/);
                if (match) {
                    if (match[1]) {
                        indent += " ";
                    }
                    indent += "- ";
                }
            }

            return indent;
        };

        this.checkOutdent = function (state, line, input) {
            return this.$outdent.checkOutdent(line, input);
        };

        this.autoOutdent = function (state, doc, row) {
            this.$outdent.autoOutdent(doc, row);
        };

        this.$id = "ace/mode/lean";
    }).call(Mode.prototype);

    exports.Mode = Mode;
});
